We use the prototype described in Section~\ref{sec:FormalVer_ConstSolvers} toverify our GM-to-AUTOSAR transformation. However, the verificationprototype can only verify ATL transformations composed of declarative matchedrules and non-recursive lazy rules. Thus we have changed the implementation describedin~\cite{ECMFApaper} to be completely declarative and compatible with theformat required by the prototype. The final reimplementation isintended to achieve the same mapping as the original implementationdescribed in~\cite{ECMFApaper}.In this section, we describe the constructs used to re-implementour transformation and the different kinds of constraintsformulated for verification.